Nuprl Lemma : comb_for_length_wf1
2,24
postcript
pdf
(
A
,
l
,
z
. ||
l
||)
A
:Type
(
A
List)
True
latex
Definitions
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
length
wf1
,
squash
wf
,
true
wf
origin
A,l,z. ||l||) 
A:Type
(A List)
True
A,l,z. ||l||) A:Type(A List)True T
x:A. B(x)T